/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     
 * Description  :     
 * Change log   :     	-Date:  Change
 ************************************************************************/

using System;
using SMLib.Interoperability.DOT;
using SMLib.Automata.Base;
using SMLib.Automata.Kripke;

namespace SMLib.Interoperability.DOT
{
	public class DotHelper_NbitKr: DotHelper<NbitKripke.State,NbitKripke.Transition>
	{

		/// <summary>
		/// Write a mealy machine into a file
		/// </summary>
		/// <param name="path">path of file</param>
		/// <param name="mm">the mealy machine</param>
		public static void WriteToDot (string path, NbitKripke mm)
		{
			DotHelper_NbitKr exporter = new DotHelper_NbitKr ();
			(exporter as DotHelper<NbitKripke.State,NbitKripke.Transition>).WriteToDot (path, mm);
		}

		/// <summary>
		/// Read a Mealy machine from a DOT file
		/// </summary>
		/// <param name="inputFile">path of file</param>
		/// <returns>the read mealy machine</returns>
		public static NbitKripke ReadFromDot (string inputFile)
		{
			NbitKripke m = new NbitKripke ();
			//m.InputAlphabet = new Alphabet();


			DotFormat dotReader = new DotFormat ();
			string ilbl;
			foreach (DotFormat.DotTransition tr in dotReader.ReadDotFile(inputFile)) {
				ilbl = tr.Label;

				if (!m.InputAlphabet.Contains (new StringSymbol (ilbl)))
					m.InputAlphabet.AddSymbol (new StringSymbol (ilbl));
				//TODO we should consistency:
				// 1-number of bits should be the same in all states
				// 2-output of state should be the same everywhere

				SMLib.Automata.Kripke.NbitKripke.State srcNode = null, dstNode = null;
				string src = tr.Source.Substring (0, tr.Source.IndexOf ("_"));
				string dst = tr.Destination.Substring (0, tr.Source.IndexOf ("_"));
				string olabelSrc = tr.Source.Substring 
					(tr.Source.IndexOf ("_") + 1, tr.Source.Length - tr.Source.IndexOf ("_") - 1);
				string olabelDst = tr.Source.Substring
					(tr.Destination.IndexOf ("_") + 1, tr.Destination.Length - tr.Destination.IndexOf ("_") - 1);
				foreach (SMLib.Automata.Kripke.NbitKripke.State n in m.GetStates()) {

					if (((string)n.Identifier).Equals (src))
						srcNode = n;
					if (((string)n.Identifier).Equals (dst))
						dstNode = n;

					if (dstNode != null && srcNode != null)
						break;
				}

				if (srcNode == null) {
					srcNode = new SMLib.Automata.Kripke.NbitKripke.State (src, new NbitSymbol (olabelSrc));
					m.AddState (srcNode);

					if (src == dst)
						dstNode = srcNode;
				}

				if (dstNode == null) {
					dstNode = new SMLib.Automata.Kripke.NbitKripke.State (dst, new NbitSymbol (olabelDst));
					m.AddState (dstNode);
				}

				SMLib.Automata.Kripke.NbitKripke.Transition t = 
					new SMLib.Automata.Kripke.NbitKripke.Transition (new StringSymbol (ilbl));
				t.SetDestination (dstNode);
				srcNode.Transitions.Add (t);
			}

			return m;
		}
	}
}

